package ss.pku.jsa.type.inference;

import java.util.Set;
import java.util.SortedSet;
import java.util.TreeSet;

import ss.pku.jsa.type.constraint.solver.Native;
import ss.pku.jsa.type.constraint.solver.QError;


@SuppressWarnings({"unchecked","rawtypes"})
public class Qualifier {
	private int nativeIndex;
	public int qualID;
	private SortedSet<String> inferredQualifiers = null;
	private String name;
	private boolean complete = false;
	boolean original;
	Qualifier javariHackShadow = this;
	public static final int VALUE_LEVEL = 0;
	public static final int REF_LEVEL = 1;

	private Qualifier(int nativeIndex) {
		this.nativeIndex = nativeIndex;
	}

	public void setGlobal(boolean global) {
		if (!this.complete) {
			throw new RuntimeException("Called setGlobal on " + this.name
					+ " before complete.");
		}
		Native.makeQvarGlobal(this.nativeIndex, global);
	}

	public void setPreferred(boolean preferred) {
		if (!this.complete) {
			throw new RuntimeException("Called setPreferred on " + this.name
					+ " before complete.");
		}
		Native.makeQvarPreferred(this.nativeIndex, preferred);
	}

	public String toString() {
		if (this.nativeIndex == 0) {
			return "null";
		}
		return (this.original ? "*" : "") + getName();
	}

	public String getName() {
		if (!this.complete)
			throw new RuntimeException("Called getName on " + this.name
					+ " before complete.");
		return this.name;
	}

	public void setName(String name) {
		if (!this.complete)
			throw new RuntimeException("Called setName on " + name
					+ " before complete.");
		Native.setQualName(this.nativeIndex, name);
		this.name = name;

		JqualPlugin.analysis.addQualifier(this);
	}

	public int getSign() {
		if (JqualPlugin.banshee) {
			return Native.signQual(this.name);
		}
		return Native.signQual(this.nativeIndex);
	}

	public int getLevel() {
		return Native.levelQual(this.nativeIndex);
	}

	public boolean isOriginal() {
		return this.original;
	}


	public Set<String> getInferredSet() {
		if (this.inferredQualifiers == null) {
			this.inferredQualifiers = new TreeSet();
			Native.getInferredQualifiers(this);
		}
		return this.inferredQualifiers;
	}

	public String getInferred() {
		StringBuffer ret = new StringBuffer(" ");

		if (JqualPlugin.inferReadonly) {
			if (isReadonly()) {
				return "readonly ";
			}
			return "mutable ";
		}
		for (String s : getInferredSet())
			ret.append(s + " ");
		return ret.toString();
	}

	public void callbackAddInferredQualifier(int nativeIndex, String name) {
		JqualPlugin.out.println("Adding " + name + " to " + this.name);
		this.inferredQualifiers.add(name);
	}

	public static Qualifier makeQualifierVariable(String name, Location loc,
			boolean original, boolean preferred, boolean global) {
		if (loc == null) {
			Profile.logMemStart("makeQualifierVariable/new Location");
			loc = new Location("unspecified location", 0L, 0L);
			Profile.logMemEnd();
		}

		int nativeIndex = CQual.makeQVar(name, loc, preferred, global);
		if (nativeIndex == 0)
			throw new Error("Native library failure in qualifier creation");
		Profile.logMemStart("makeQualifierVariable/new Qualifier");
		Qualifier q = new Qualifier(nativeIndex);
		Profile.logMemEnd();
		q.original = original;
		q.name = name;
		q.complete = true;
		JqualPlugin.analysis.addQualifier(q);
		return q;
	}

	public static Qualifier makeQualifierVariable(String name, Location loc,
			boolean original) {
		return makeQualifierVariable(name, loc, original, true, false);
	}

	public int getNativeIndex() {
		return this.nativeIndex;
	}

	public boolean isVariable() {
		return Native.variableQual(this.nativeIndex);
	}

	public boolean isConstant() {
		return Native.constantQual(this.nativeIndex);
	}

	public static Qualifier findQualifierConstant(String name) {
		while ((name.length() > 0) && (name.charAt(name.length() - 1) == '*')) {
			name = name.substring(0, name.length() - 1);
		}

		Qualifier q = JqualPlugin.analysis.getQualifierConstant(name);
		if (q != null) {
			return q;
		}

		int nativeIndex = Native.findQual(name);

		if (nativeIndex == 0) {
			JqualPlugin.out.println("native qualifier constant '" + name
					+ "' not found");
			return null;
		}

		Profile.logMemStart("findQualifierConstant/new Qualifier");
		q = new Qualifier(nativeIndex);
		Profile.logMemEnd();
		q.original = true;
		q.name = name;

		q.complete = true;
		JqualPlugin.analysis.putQualifierConstant(name, q);
		return q;
	}

	public void makeConservativeAssumptions(boolean contravariant) {
		if (!JqualPlugin.inferReadonly)
			return;
		Location l = Location.getConservativeAssumptionLocation();
		if ((!this.name.equals("Object_cons_ret")) || (contravariant)) {
			makeMutable(l, QError.JAVARI_CONSERV);
		} else {
			Qualifier cq = JqualPlugin.analysis.readonly;
			CQual.makeEdge(Constraint.Kind.LT, cq, this, QualGate.EMPTY, l, 0,
					QError.JAVARI_CONSERV);
		}
	}

	public boolean equals(Object o) {
		if (!(o instanceof Qualifier))
			return false;
		Qualifier q = (Qualifier) o;
		return q.nativeIndex == this.nativeIndex;
	}

	public int hashcode() {
		return this.nativeIndex;
	}

	public boolean isReadonly() {
		if (JqualPlugin.useJavariSelfLoopsHack) {
			return !Native.leqQual(this.javariHackShadow.nativeIndex,
					JqualPlugin.analysis.mutable.nativeIndex);
		}
		return !Native.leqQual(this.nativeIndex,
				JqualPlugin.analysis.mutable.nativeIndex);
	}

	public void makeMutable(Location l, QError error) {
		if (JqualPlugin.useJavariSelfLoopsHack) {
			Qualifier dummy = makeQualifierVariable(this.name + "_shadow", l,
					false);
			dummy.setGlobal(true);
			CQual.makeEdge(Constraint.Kind.LT, this, dummy, QualGate.EMPTY, l,
					0, error);
			CQual.makeEdge(Constraint.Kind.LT, dummy,
					JqualPlugin.analysis.mutable, QualGate.EMPTY, l, 0, error);
		} else {
			CQual.makeEdge(Constraint.Kind.LT, this,
					JqualPlugin.analysis.mutable, QualGate.EMPTY, l, 0, error);
		}
	}

	public void makeJavariHackShadowLT(Location l) {
		Qualifier shadow = makeQualifierVariable(getName() + "_shadow", l,
				false, false, true);
		CQual.makeEdge(Constraint.Kind.LT, shadow, this, QualGate.EMPTY, l, 0,
				QError.JAVARI_GLOBAL_HACK);
		this.javariHackShadow = shadow;
	}
}
